perm filename CYCLE.LSP[F81,JMC]1 blob
sn#619409 filedate 1981-10-17 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 (proof cycle)
C00013 ENDMK
C⊗;
(proof cycle)
(setq condflag nil)
(decl (x y z x1 x2 x3 y1 y2 y3 z1 z2 z3) |ground| variable sexp)
(decl (a b c a1 a2 b1 b2 c1 c2) | ground| variable atom)
(decl (tt nnil) |ground | constant atom)
(decl (g g1 g2 g3) |ground| variable)
(decl (car cdr) |ground→ground| constant)
(decl (cons) |ground⊗ground →ground| constant)
(decl (phi) |ground→truthval| variable)
(axiom |∀g. atom(g)⊃sexp(g)|)
(axiom |∀x y.sexp(cons(x,y))|)
(axiom |∀g .sexp(g) ⊃ (atom(g) ∨ ∃x y. g=cons(x,y))|)
(axiom |∀x y. ¬atom(cons(x,y))|)
(axiom |∀x y.car(cons(x,y))=x|)
(axiom |∀x y.cdr(cons(x,y))=y|)
(axiom |∀phi.(∀a.phi(a) ∧ ∀x y.(phi(x)∧phi(y)⊃phi(cons(x,y))) ⊃∀ x.phi(x))|)
(decl (u v w u1 u2 u3 v1 v2 v3 w1 w2 w3) |ground| variable list)
(decl (null) |ground→truthval|)
(axiom |null(nnil)|)
(axiom |∀u.null(u)≡u=nnil|)
(axiom |list(nnil)|)
(axiom |∀g. list(g)⊃sexp(g)|)
(axiom |∀x u. ¬null(cons(x,u))|)
(DECL (*) |GROUND⊗GROUND→GROUND| CONSTANT UNIVERSAL INFIX 990)
(decl (reverse) |ground→ground| constant)
(decl (rdc) |ground⊗ground→ground|constant)
(decl (rac) |ground⊗ground→ground|constant)
(decl (snoc) |ground⊗ground→ground|constant)
(axiom |∀x u.rdc(x,u)= if null(u) then nnil else cons(x,rdc(car(u),cdr(u)))|)
(axiom |∀x u.rac(x,u)= if null(u) then x else rac(car(u),cdr(u))|)
(axiom |∀x u.snoc(x,u) = if null(u) then cons(x,nnil) else cons(car(u),
snoc(x,cdr(u)))|)
(axiom |∀u v.reverse(u*v) = reverse(v)*reverse(u)|)
(axiom |∀x.reverse(cons(x,nnil)) = cons(x,nnil)|)
(axiom |reverse(nnil) = nnil|)
(axiom |u*v = if null(u) then v else cons(car(u),cdr(u)*v)|)
(decl (h) |ground⊗ground→ground|)
(decl (drec) |ground⊗(ground⊗ground→ground)→(ground→ground)| constant)
(axiom |∀v h.(∀u v.¬null(u) ⊃ list(h(u,v))) ⊃ ∀u.list((drec(v,h))(u))|)
(axiom |∀v h.(∀u v.¬null(u) ⊃ list(h(u,v)))
⊃ (∀u.(drec(v,h))(u) = if null(u) then v else h(u,(drec(v,h))(cdr(u))))|)
(decl (app) |ground⊗ground→ground| constant)
(axiom |∀u v.app(u,v) = (drec(v,λu w.cons(car(u),w)))(u)|)
(∀e v v 36)
(∀e h |λu w.cons(car(u),w)|)
(∀e v v 37)
(∀e h |λu w.cons(car(u),w)|)
(rewrite left 43 39)
(axiom |app = λu v.(drec(v,λu w.cons(car(u),w)))(u)|)
(rewrite left 44 45)
switched to CYCLE
*
*
*
*
*
*
*
*
* 8. ∀G.ATOM(G)⊃SEXP(G)
ctxt: (1 2 4) deps: NIL
* 9. ∀X Y.SEXP(CONS(X,Y))
ctxt: (1 6) deps: NIL
* 10. ∀G.SEXP(G)⊃ATOM(G)∨(∃X Y.G=CONS(X,Y))
ctxt: (1 2 4 6) deps: NIL
* 11. ∀X Y.¬ATOM(CONS(X,Y))
ctxt: (1 2 6) deps: NIL
* 12. ∀X Y.CAR(CONS(X,Y))=X
ctxt: (1 5 6) deps: NIL
* 13. ∀X Y.CDR(CONS(X,Y))=Y
ctxt: (1 5 6) deps: NIL
* 14. ∀PHI A.PHI(A)∧(∀X Y.(PHI(X)∧PHI(Y)⊃PHI(CONS(X,Y)))⊃(∀X.PHI(X)))
ctxt: (1 2 6 7) deps: NIL
*
*
* 17. NULL(NNIL)
ctxt: (3 16) deps: NIL
* 18. ∀U.NULL(U)≡U=NNIL
ctxt: (3 15 16) deps: NIL
* 19. LIST(NNIL)
ctxt: (3 15) deps: NIL
* 20. ∀G.LIST(G)⊃SEXP(G)
ctxt: (1 4 15) deps: NIL
* 21. ∀X U.¬NULL(CONS(X,U))
ctxt: (1 6 15 16) deps: NIL
*
*
*
*
*
* 27. ∀X U.RDC(X,U)=IF NULL(U) THEN NNIL ELSE CONS(X,RDC(CAR(U),CDR(U)))
ctxt: (1 3 5 6 15 16 24) deps: NIL
* 28. ∀X U.RAC(X,U)=IF NULL(U) THEN X ELSE RAC(CAR(U),CDR(U))
ctxt: (1 5 15 16 25) deps: NIL
* 29. ∀X U.SNOC(X,U)=IF NULL(U) THEN CONS(X,NNIL) ELSE CONS(CAR(U),SNOC(X,CDR(U)))
ctxt: (1 3 5 6 15 16 26) deps: NIL
* 30. ∀U V.REVERSE(U*V)=REVERSE(V)*REVERSE(U)
ctxt: (15 22 23) deps: NIL
* 31. ∀X.REVERSE(CONS(X,NNIL))=CONS(X,NNIL)
ctxt: (1 3 6 23) deps: NIL
* 32. REVERSE(NNIL)=NNIL
ctxt: (3 23) deps: NIL
* 33. U*V=IF NULL(U) THEN V ELSE CONS(CAR(U),CDR(U)*V)
ctxt: (5 6 15 16 22) deps: NIL
*
*
* 36. ∀V H.(∀U V.¬NULL(U)⊃LIST(H(U,V)))⊃(∀U.LIST((DREC(V,H))(U)))
ctxt: (15 16 34 35) deps: NIL
* 37. ∀V H.(∀U V.¬NULL(U)⊃LIST(H(U,V)))⊃
(∀U.(DREC(V,H))(U)=IF NULL(U) THEN V ELSE H(U,(DREC(V,H))(CDR(U))))
ctxt: (5 15 16 34 35) deps: NIL
*
* 39. ∀U V.APP(U,V)=(DREC(V,λU W.CONS(CAR(U),W)))(U)
ctxt: (5 6 15 35 38) deps: NIL
* 40. ∀H.(∀U V.¬NULL(U)⊃LIST(H(U,V)))⊃(∀U.LIST((DREC(V,H))(U)))
ctxt: (15 16 34 35) deps: NIL
* 41. (∀U V.¬NULL(U)⊃LIST(CONS(CAR(U),V)))⊃
(∀U.LIST((DREC(V,λU W.CONS(CAR(U),W)))(U)))
ctxt: (5 6 15 16 35) deps: NIL
* 42. ∀H.(∀U V.¬NULL(U)⊃LIST(H(U,V)))⊃
(∀U.(DREC(V,H))(U)=IF NULL(U) THEN V ELSE H(U,(DREC(V,H))(CDR(U))))
ctxt: (5 15 16 34 35) deps: NIL
* 43. (∀U V.¬NULL(U)⊃LIST(CONS(CAR(U),V)))⊃
(∀U.(DREC(V,λU W.CONS(CAR(U),W)))(U)=
IF NULL(U) THEN V
ELSE CONS(CAR(U),(DREC(V,λU W.CONS(CAR(U),W)))(CDR(U))))
ctxt: (5 6 15 16 35) deps: NIL
* 44. (∀U V.¬NULL(U)⊃LIST(CONS(CAR(U),V)))⊃
(∀U.APP(U,V)=
IF NULL(U) THEN V
ELSE CONS(CAR(U),(DREC(V,λU W.CONS(CAR(U),W)))(CDR(U))))
ctxt: (5 6 15 16 35 38) deps: NIL
* 45. APP=(λU V.(DREC(V,λU W.CONS(CAR(U),W)))(U))
ctxt: (5 6 15 35 38 deps: NIL
* 46. (∀U V.¬NULL(U)⊃LIST(CONS(CAR(U),V)))⊃
(∀U.APP(U,V)=
IF NULL(U) THEN V
ELSE CONS(CAR(U),(DREC(V,λU W.CONS(CAR(U),W)))(CDR(U))))
ctxt: (5 6 15 16 35 38) deps: NIL
*
(axiom |∀u v.app(u,v) = (drec(v,λu w.cons(car(u),w)))(u)|)
* 39. ∀U V.APP(U,V)=(DREC(V,λU W.CONS(CAR(U),W)))(U)
(∀e u |cdr(u)| 39)
* 47. LIST(CDR(U))⊃(∀V.APP(CDR(U),V)=(DREC(V,λU W.CONS(CAR(U),W)))(CDR(U)))
ctxt: (5 6 15 35 38) deps: NIL
(assume |list(cdr(u))|)
48. LIST(CDR(U))
ctxt: (5 15) deps: (48)
(⊃e 47 48)
49. ∀V.APP(CDR(U),V)=(DREC(V,λU W.CONS(CAR(U),W)))(CDR(U))
ctxt: (5 6 15 35 38) deps: (48)
(∀e v)
50. APP(CDR(U),V)=(DREC(V,λU W.CONS(CAR(U),W)))(CDR(U))
ctxt: (5 6 15 35 38) deps: (48)
(⊃i 48 50)
* 51. LIST(CDR(U))⊃APP(CDR(U),V)=(DREC(V,λU W.CONS(CAR(U),W)))(CDR(U))
ctxt: (5 6 15 35 38) deps: NIL
(rewrite left 46 51)
52. (∀U4 V4.¬NULL(U4)⊃LIST(CONS(CAR(U4),V4)))⊃
(∀U5.APP(U5,V)=
IF NULL(U5) THEN V
ELSE CONS(CAR(U5),(DREC(V,λU6 W.CONS(CAR(U6),W)))(CDR(U5))))
ctxt: (5 6 15 16 35 38 52) deps: NIL
(deletel)
(save-proofs cycle)
* 52. (∀U4 V4.¬NULL(U4)⊃LIST(CONS(CAR(U4),V4)))⊃
(∀U5.APP(U5,V)=
IF NULL(U5) THEN V
ELSE CONS(CAR(U5),(DREC(V,λU6 W.CONS(CAR(U6),W)))(CDR(U5))))
ctxt: (5 6 15 16 35 38 52) deps: NIL
* ;SAVEPROOFS UNDEFINED FUNCTION OBJECT
QUIT
* .....done.
*